$\forall$${\it da}$:$z$:Knd fp$\rightarrow$ Type, $k$:Knd. Valtype(${\it da}$;$k$) $\in$ Type